Skip to content

Feature exception#806

Open
lyonel2017 wants to merge 2 commits intomainfrom
feature-exception
Open

Feature exception#806
lyonel2017 wants to merge 2 commits intomainfrom
feature-exception

Conversation

@lyonel2017
Copy link
Contributor

@lyonel2017 lyonel2017 commented Sep 9, 2025 •
edited
Loading

This PR introduce exceptions for Hoare Logic.

We can define exception :

exception assume.
exception assert.

We can raise exception using raise assume or if (x = 3) else raise assert (raise an exception when a condition is not true):

module M ={
  proc f (x:int) : int = {
    if (x = 3) else raise assert;
    x <- 1;
    if (x = 3)  {
       raise assume;
    }
    if (x=3) {
        raise assert;
      }
  return x;
  }
}.

We can define postconditions for each exception and a default postcondition:

lemma assume_assert : hoare [M.f : pre ==> post | assume:p1 |assert: p2 | p3].

Examples are available in examples/exception.ec.

@lyonel2017 lyonel2017 force-pushed the feature-exception branch 2 times, most recently from 415a5d1 to b415379 Compare September 21, 2025 19:49
@lyonel2017 lyonel2017 requested a review from strub September 21, 2025 19:49
@lyonel2017 lyonel2017 force-pushed the feature-exception branch 4 times, most recently from b717865 to 7e145ca Compare September 22, 2025 20:48
@lyonel2017 lyonel2017 force-pushed the feature-exception branch 4 times, most recently from cac4299 to 8a1385e Compare October 3, 2025 09:53
@lyonel2017 lyonel2017 force-pushed the feature-exception branch 2 times, most recently from 1185838 to ee89281 Compare November 1, 2025 11:50
@lyonel2017 lyonel2017 force-pushed the feature-exception branch 2 times, most recently from ae978f0 to 2fa2c24 Compare December 19, 2025 17:25
@lyonel2017 lyonel2017 force-pushed the feature-exception branch 2 times, most recently from ee9b68e to 2719b38 Compare December 23, 2025 18:16
@lyonel2017 lyonel2017 marked this pull request as ready for review December 23, 2025 18:45
@lyonel2017 lyonel2017 requested a review from bgregoir December 23, 2025 18:45
bgregoir
bgregoir reviewed Dec 25, 2025
View reviewed changes
@lyonel2017 lyonel2017 force-pushed the feature-exception branch 3 times, most recently from 1397fe3 to 7f90d68 Compare December 30, 2025 18:13
lyonel2017
lyonel2017 commented Jan 15, 2026
View reviewed changes
src/ecHiInductive.ml
val create : EcPath.path list list -> t
val add : (int * locals) list -> expr -> t -> bool
val resolve : t -> opbranches option
val resolve : t -> opbranches
Copy link
Contributor Author

@lyonel2017 lyonel2017 Jan 15, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't understand these changes.

@lyonel2017 lyonel2017 force-pushed the feature-exception branch 2 times, most recently from db8c743 to 5ff2221 Compare January 16, 2026 16:43
@lyonel2017 @bgregoir @strub
Add exception declaration, raise, and update logic
342576e 
Co-Authored-By: Benjamin Gregoire <[email protected]>
Co-Authored-By: Pierre-Yves Strub <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@bgregoir bgregoir bgregoir left review comments

@strub strub Awaiting requested review from strub

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@lyonel2017 @bgregoir